console.profile(); //start firefox javascript profiler

/*

Mikhail Breslav and Chris Kwan
{breslav, ckwan}@cs.bu.edu
http://cs-people.bu.edu/ckwan/cs511/

CS 511 Spring 2011 Project
Client-side Parsing and Verification

Parser for Propositional Logic

Last update: 05/10/2011

*/


/*
 Initialize text areas and class variables
*/    

var message = "Assume: [p]\nAssume: [q]\nAssert: not [p] and [q] implies ( [p] or [q] )\n"
var instructions = $("instructionsBox");
instructions.value = message;

$("inputBox").focus();
$("inputBox").value = "";


var expressionString = ""; //the expression string being parsed, most methods reference this
var assertionExpression;

var originalStr = "";
var originalStrCopy = "";
var formulaStr = "";
var formulaStrCopy = "";
var formulaTable = new hash_atoms();
var truthTable;
var parseTreeStr = "";
var numCounterEx = 0; //number of counter examples (assignments resulting in false in truth table)

var truthTableNotInitVal = -1;
var startingTruthValue = true;
var numWordsInTable = 0;

var notSym = "not";
var andSym = "and";
var orSym = "or";
var impliesSym = "implies";
var groupLeftSym = "(";
var groupRightSym = ")";
var wordLeftSym = "[";
var wordRightSym = "]";

var green = "#CCFFCC";
var red = "#FF9999";
var yellow = "#FFFFCC";
var white = "#FFFFFF";

var assertPropsArray = new Array();

var outputs = new Array(); //outputs means the outputs for the different assignments that we evaluate to check whether something is a tautology.


/*
 Shortcut to get a document element by id.
*/
function $(id)
{
    return document.getElementById(id);
}


/*
 Clear out the values in the output and debug text boxes.
*/
function clearBoxes()
{
    parseTreeStr = "";
    
    formulaTable.clear(); //table of words
    numWordsInTable = 0;
    numCounterEx = 0;
	
	//remove all elements from the assert div
	var assertDiv = $("assertDiv");
	if( assertDiv.hasChildNodes() )
	{
		while (assertDiv.childNodes.length > 0 )
		{
			assertDiv.removeChild( assertDiv.firstChild );
		}
	}
	
    //clear out the details section
    clearAssertDetails();
    
    //clear error div
    clearChildren("errorDiv");
    
    //clear assert div
    clearChildren("assertDiv");
}


function clearChildren(parentName)
{
var clearDiv = $(parentName);
	if( clearDiv.hasChildNodes() )
	{
		while (clearDiv.childNodes.length > 0 )
		{
			clearDiv.removeChild( clearDiv.firstChild );
		}
	}
	
}

/*
 Call update method if user presses Shift+Enter.
*/
function keypress(key)
{
    var code = key.charCode;
    if( code == 0 || code == undefined)
        code = key.keyCode;
        
    if(code == 13 && key.shiftKey)
        update();
}    


/*
 Pass the argument from the input box to the parser.
*/
function update()
{
    var input = $("inputBox").value;
    
    originalStr = input;
    originalStrCopy = originalStr;
    
    clearBoxes();
    
    parseArgument();
}


/*
 Clear the text in the input box.
*/
function clearInput()
{
    $("inputBox").value = "";
    clearBoxes();
}
    
    
/*
 Parse an argument (assumptions and assertions) and display if each assertion is valid or invalid.
*/
function parseArgument()
{
	var premises = "";
	var firstWord = "";
	var firstChar = "";
	var tempAssertion = "";
	var tempPremise = "";
	var isTauto = false;
	var assertIndex = 0;
	
    clearChildren("assertDiv");
	$("assertDiv").innerHTML += "<h2>Assertions:</h2>";
	
	originalStrCopy = skipLeadingBlanks(originalStrCopy); //skip initial blanks
	
    //process all text in input box until it is empty
	while(originalStrCopy.length > 0)
	{
		isTauto = false;		
		
        firstWord = getFirstWord(originalStrCopy);

        //if we have an assumption
        if( firstWord == "assume:" || firstWord == "Assume:" 
            || firstWord == "assume" || firstWord == "Assume" )
        {
            originalStrCopy = chompOffFirstWord(originalStrCopy);
            originalStrCopy = skipLeadingBlanks(originalStrCopy);
            var tempChar = getFirstChar(originalStrCopy);
            tempPremise = "";
        
            while(tempChar != "\n" && !(originalStrCopy.length == 0) )
            {
                tempPremise += tempChar;
                originalStrCopy = chompOffFirstChar(originalStrCopy);
                tempChar = getFirstChar(originalStrCopy);
            }
            
            originalStrCopy = skipLeadingBlanks(originalStrCopy);
        
            tempPremise = groupLeftSym + tempPremise + groupRightSym;
            
            if(premises.length > 0)
            {
                premises = premises + " " + andSym + " " + tempPremise;
            }
            else
            {
                premises = tempPremise;
            }
        }//end if assume
        
        else //if we have an assertion
        {
            //if the user actually used the word "assert"
            if( firstWord == "assert:" || firstWord == "Assert:"
                || firstWord == "assert" || firstWord == "Assert" )
            {
            // we have an assertion
            originalStrCopy = chompOffFirstWord(originalStrCopy);
            }
            
            originalStrCopy = skipLeadingBlanks(originalStrCopy);
            var tempChar = getFirstChar(originalStrCopy);
            tempAssertion = "";
        
            while(tempChar != "\n" && !(originalStrCopy.length == 0) )
            {
                tempAssertion += tempChar;
                originalStrCopy = chompOffFirstChar(originalStrCopy);
                tempChar = getFirstChar(originalStrCopy);
            }
            originalStrCopy = skipLeadingBlanks(originalStrCopy);
            
			var assertDetails = document.createTextNode( assertIndex +": " + tempAssertion + "\n" );
			
			var assertLink = document.createElement("button");
			assertLink.setAttribute("onclick", "updateAssertDetails(\"" + tempAssertion + "\")" );
			assertLink.appendChild( document.createTextNode("Show Details") );
			
            
			$("assertDiv").appendChild(assertDetails);
			
            //now we want to see whether (premises list) implies (assertion)
            if(premises == "")
            {
                formulaStr = tempAssertion;
            }
            else
            {
                formulaStr = premises + " " + impliesSym + " " + groupLeftSym + tempAssertion + groupRightSym;
            }
            
            
			//make a copy of the formula string since it will get modified by the parser
            formulaStrCopy = formulaStr;
            
            //call the parser once initially to find out how many words there are (make word table)
            cleanupBeforeAssignment();	
            expressionValue(0, truthTableNotInitVal);
            cleanupAfterAssignment();
			
            //generate truth table using the word table
            printTruthTable(formulaTable); 
            
            //print out truth table
            debugPrintTruthTable();
            
            //check if formula is a tautology using the truth table
            isTauto = isFormulaTautology();
			
			
			assertPropsArray[tempAssertion] = new Array();
			
			assertPropsArray[tempAssertion]["assumptions"] = premises;
			assertPropsArray[tempAssertion]["assertion"] = tempAssertion;
			
			//copy each of the arrays inside of truthTable (an array of arrays)
			var truthTableCopy = new Array();
			for(tti = 0; tti < truthTable.length; tti++)
			{
				truthTableCopy[tti] = new Array();
				for(ttj = 0; ttj < truthTable[tti].length; ttj++)
				{
					truthTableCopy[tti][ttj] = truthTable[tti][ttj];
				}
			}
			assertPropsArray[tempAssertion]["truthtable"] = truthTableCopy;
	
			assertPropsArray[tempAssertion]["outputs"] = outputs.slice();
			
			assertPropsArray[tempAssertion]["parseTree"] = parseTreeStr;
			
            assertPropsArray[tempAssertion]["numCounterEx"] = numCounterEx;
			
			assertIndex++;
			
            if(isTauto)
            {
                //assertionsBox.value += " VALID\n";				
				$("assertDiv").innerHTML += "<span style=\"background-color: " + green + "\"> " + " VALID " + "</span>";
            }
            else
            {
                //assertionsBox.value += " INVALID\n";
				$("assertDiv").innerHTML += "<span style=\"background-color: " + red + "\"> " + " INVALID " + "</span>";
            }
			
			$("assertDiv").appendChild( assertLink );
			$("assertDiv").appendChild( document.createElement("br") );
			
            
        }//end else assert
        
	}//end while
    
}//end parseArgument


/*
 Clear all the info in the Details section
*/
function clearAssertDetails()
{
    clearChildren("detailsTitleDiv");
    clearChildren("assumeDiv");   
    clearChildren("currentAssertionDiv");
    clearChildren("implicationDiv");
    clearChildren("summaryDiv");
    clearChildren("truthtableDiv");
    clearChildren("parseTreeDiv");
}

/*
 Update all of the assert detail boxes with information for this assertion.
*/
function updateAssertDetails(assertion)
{
    //write Details title
    clearChildren("detailsTitleDiv");
    //add Hide Details Button
    $("detailsTitleDiv").innerHTML += "<br>";
    $("detailsTitleDiv").innerHTML += "<button onclick = clearAssertDetails()>Hide Details</button>";
    $("detailsTitleDiv").innerHTML += "<h2>Details:</h2>";


	//current assumptions
	clearChildren("assumeDiv");
    $("assumeDiv").innerHTML += "<h3>Assumptions:</h3>";
	var assumptionsText = assertPropsArray[assertion]["assumptions"];
	$("assumeDiv").appendChild(document.createTextNode(assumptionsText));
	
	//current assertion
	clearChildren("currentAssertionDiv");
	$("currentAssertionDiv").innerHTML += "<h3>Assertion:</h3>";
    var assertionText = assertPropsArray[assertion]["assertion"];
	$("currentAssertionDiv").appendChild(document.createTextNode(assertionText));
	
    //implication (assumptions -> assertion)
    clearChildren("implicationDiv");
    $("implicationDiv").innerHTML += "<h3>Implication (Assumptions -> Assertion):</h3>";
    
    if(assumptionsText.length > 0)
    {
        $("implicationDiv").innerHTML += assumptionsText;
        $("implicationDiv").innerHTML += " implies ";
    }
    
    $("implicationDiv").innerHTML += assertionText;
    
    //summary
    var myNumCounterEx = assertPropsArray[assertion]["numCounterEx"];
    var myNumAssn = assertPropsArray[assertion]["truthtable"].length;
    
    clearChildren("summaryDiv");
    $("summaryDiv").innerHTML += "<h3>Summary:</h3>";
    
    var summaryText = "";
    $("summaryDiv").innerHTML += "# of Counter-Examples: " + myNumCounterEx + "<br>";
    $("summaryDiv").innerHTML += "# of Assignments: " + myNumAssn + "<br>";
    
    if(myNumCounterEx < myNumAssn)
    {
        $("summaryDiv").innerHTML += 
            "Satisfiable (at least one assignment evaluates to true)" + "<br>";
    }
    
    if(myNumCounterEx == myNumAssn)
    {
        $("summaryDiv").innerHTML += "Contradiction (all assignments evaluate to false)" + "<br>";
    }
    else if(myNumCounterEx == 0)
    {
        $("summaryDiv").innerHTML += "Tautology (all assignments evaluate to true)" + "<br>";
    }
    
    //truth table
	var truthtableTemp= assertPropsArray[assertion]["truthtable"];
	var tempOutput = assertPropsArray[assertion]["outputs"];
	clearChildren("truthtableDiv");
	$("truthtableDiv").innerHTML += "<h3>Truth Table:</h3>";
    
	for(i=0; i< truthtableTemp.length; i++)
	{
	
		var tempRowStr = "";
		
		tempRowStr += i + "\t: ";
		for(j = 0; j< truthtableTemp[i].length ; j++)
		{
			if(truthtableTemp[i][j] == false)
			{
				tempRowStr += "F ";
			}
			else if(truthtableTemp[i][j] == true)
			{
				tempRowStr +=  "T ";
			}
			else
			{
				tempRowStr += " $  ";
			}
		} //end of inner for
					
		tempRowStr += "| " + tempOutput[i] + " \n";	
		
		var color;
		
		if(tempOutput[i] == false)
		{
			color = red;
		}
		else if(tempOutput[i] == true)
		{
			color = green;
		}
		else
		{
			color = yellow;
		}
		
		$("truthtableDiv").innerHTML += "<span style=\"background-color: " + color + "\">" +  tempRowStr + "</span>" + "<br>";
	} //end of outer for
			
            
	//parse tree		
	var myParseTreeStr = assertPropsArray[assertion]["parseTree"];
	
	clearChildren("parseTreeDiv");
    $("parseTreeDiv").innerHTML += "<h3>Parse Tree:</h3>";
    
    //add a textbox to parseTreeDiv so we can display newlines correctly
    var textAreaNode = document.createElement("textarea");
    textAreaNode.setAttribute("rows", "20");
    textAreaNode.setAttribute("cols", "50");
    textAreaNode.appendChild(document.createTextNode(myParseTreeStr));
	$("parseTreeDiv").appendChild(textAreaNode);
}


/*
 Do some cleanup before running the parser.
*/
function cleanupBeforeAssignment()
{
    //clear debug box (parse tree)
    parseTreeStr = "";
	formulaTable.clear(); //table of words
	numWordsInTable = 0;
}


/*
 Do some cleanup after running the parser, in preparation for the next run.
*/
function cleanupAfterAssignment()
{
    //restore formulaStr
    formulaStr = formulaStrCopy;
}


/*
 Print out the already generated truth table.
*/
function debugPrintTruthTable()
{
	var numWords = formulaTable.length;
    var numAssignments = Math.pow(2,numWords);

    var table = formulaTable;
    
    //add a title row with word names to the printout
    var titles = "";
    for(var word in table.items)
    {
        titles += word + "\t|";
    }
    
    //print a slight underline
    var underLine = "";
    for(var word in table.items)
    {
        underLine += "__" + "\t|";
    }
    
    //print out the truth values
    for(i=0; i<numAssignments; i++)
	{
        //truthTableBox.value += i + ": ";
        
		for(j=0; j<numWords; j++)
		{
			//truthTableBox.value += truthTable[i][j] + " ";
		}
		
		//truthTableBox.value += "\n";
	}

}


/*
 Return true if the formula is a tautology (true for all possible assignments of variables)
*/
function isFormulaTautology()
{
    //assuming truth table already generated
    var isTaut = true;
    
    var numAssn = truthTable.length;
    
    numCounterEx = 0;
    
    var value;
    //evaluate every assignment (row)
    for(i=0; i<numAssn; i++)
    {
        cleanupBeforeAssignment();
        
        value = expressionValue(0, i);
        
		outputs[i] = value;
		
        cleanupAfterAssignment();
        
        if(value == false)
        {
            //add to counterexamples
            numCounterEx++;
            
            isTaut = false;
            //don't break, instead keep going to list all counterexamples
        }
        //if true keep going
    }//end for  
    
    if(isTaut)
    {
        return true;
    }
    else
    {
        return false;
    }
}//end isFormulaTautology


/*
 Generate a truth table given a table of words (titles).
*/
function printTruthTable(table)
{
    var numWords = table.length;
	var numAssignments = Math.pow(2,numWords);

	truthTable = new Array(numAssignments);
    
    //initialize 2D Array
    //each row is an assignment
    //and each column is a word
    for(i=0; i<numAssignments; i++)
	{
        truthTable[i] = new Array(numWords);
	}

    //add a title row with word names to the printout
    var titles = "";
    for(var word in table.items)
    {
        titles += word + "\t|";
    }
    //truthTableBox.value += titles + "\n";
    
    //print a slight underline
    var underLine = "";
    for(var word in table.items)
    {
        underLine += "__" + "\t|";
    }
    //truthTableBox.value += underLine + "\n";

    //reset current assignment Number
    curAssnNum = 0;
    
    printTruthTableHelper(0,"",numWords);
}


//variables for generating truth table
var itemValsArray = new Array(); //holds truth values of current row in table
var curAssnNum = 0; //holds the current assignment number (row in truth table being filled in)


/*
 Helper method for recursively generating all the truth values in the truth table.
*/
function printTruthTableHelper(curItemIndex, strSoFar, numItems)
{
    var numTruthVals = 2; //0 and 1
    
    //at the last column of the table, print out the row
    if(curItemIndex == numItems-1)
    {
        for(var k=0; k<numTruthVals; k++)
        {
            var truthVal;
            if(k==0)
            {
                truthVal = false;
            }
            else if(k==1)
            {
                truthVal = true;
            }
            truthTable[curAssnNum][curItemIndex] = truthVal;
            
            //display the current assignment
            var truthStr;
            truthStr = truthTable[curAssnNum][curItemIndex];
            //truthTableBox.value += strSoFar + truthStr + "\t|" + "\n";
            
            //store the current row in the truth table
            for(var i=0; i<curItemIndex; i++)
            {
                truthTable[curAssnNum][i] = itemValsArray[i];
            }
            
            //update for the next assignment
            curAssnNum++;
        }
    }
    else if(curItemIndex < numItems-1)
    {
        for(var j=0; j<numTruthVals; j++)
        {
            var truthVal;
            if(j==0)
            {
                truthVal = false;
            }
            else if(j==1)
            {
                truthVal = true;
            }
            truthTable[curAssnNum][curItemIndex] = truthVal;
            
            //add truth value to display for current assignment
            var truthStr;
            truthStr = truthTable[curAssnNum][curItemIndex];
                
            //add truth value to item vals Array
            itemValsArray[curItemIndex] = truthVal;
            
            //call on the next word in the row
            printTruthTableHelper( curItemIndex+1, 
                (strSoFar + truthStr + "\t|"), numItems, curAssnNum);
                
        }//end for
    }//end else if
    else //curItemIndex > numItems - 1
    {
        updateErrorBox("error generating truth table, " 
            + "curItemIndex: " + curItemIndex
            + "numItems - 1: " + numItems-1 );
    }
}


/*
 Return the truth value of an expression.
*/
function expressionValue(numTabs, assnIndex)
{
    parseTreeStr += createTabs(numTabs) + "<expression>" + "\n";

    var value;
    
    formulaStr = skipLeadingBlanks(formulaStr);
    
    value = termValue(numTabs+1, assnIndex);
    
    formulaStr = skipLeadingBlanks(formulaStr);
    
    var nextWord = getFirstWord(formulaStr);
    
    if(nextWord == impliesSym)
    {
        parseTreeStr += createTabs(numTabs+1) + "\"" + nextWord +"\"" + "\n";
        
        //remove the word implies
        formulaStr = chompOffFirstWord(formulaStr);
        
        var expressionVal = expressionValue(numTabs+1, assnIndex);
        
        //value -> expressionVal
        //= (not value) or expressionVal
        value = (!value || expressionVal);
    }
 
    parseTreeStr += createTabs(numTabs) + "</expression>" + "\n";
    
    return value;
}//end expressionValue


/*
 Return the truth value of a term.
*/
function termValue(numTabs, assnIndex)
{
    parseTreeStr += createTabs(numTabs) + "<term>" + "\n";
    
    var value;
    
    formulaStr = skipLeadingBlanks(formulaStr);
    
    value = factorValue(numTabs+1, assnIndex);
    
    formulaStr = skipLeadingBlanks(formulaStr);
    
    var nextWord = getFirstWord(formulaStr);
    
    //keep checking for more factors connected with "and" or "or"
    while(nextWord == andSym || nextWord == orSym)
    {
        //remove the and, or
        formulaStr = chompOffFirstWord(formulaStr);
        
        parseTreeStr += createTabs(numTabs+1) 
            + "\"" + nextWord + "\"" + "\n";
        
        var nextValue = factorValue(numTabs+1, assnIndex);
        
        if(nextWord == andSym)
        {
            value = value && nextValue;
        }
        else //or
        {
            value = value || nextValue;
        }
        
        formulaStr = skipLeadingBlanks(formulaStr);
        
        nextWord = getFirstWord(formulaStr);
    }
    
    parseTreeStr += createTabs(numTabs) + "</term>" + "\n";
    
    return value;
    
}//end termValue


/*
 Return the truth value of a factor.
*/
function factorValue(numTabs, assnIndex)
{
    parseTreeStr += createTabs(numTabs) + "<factor>" + "\n";
    
    var value;
    var isNegated = false;
    
    formulaStr = skipLeadingBlanks(formulaStr);
    
    //check for the word not
    var nextWord = getFirstWord(formulaStr);    
    if(nextWord == notSym)
    {
        parseTreeStr += createTabs(numTabs+1) 
            + '"' + notSym + '"' + "\n";
         
        //remove the word not
        formulaStr = chompOffFirstWord(formulaStr);
        
        isNegated = true;
    }
    
    //in case we removed a not, remove the space after not
    formulaStr = skipLeadingBlanks(formulaStr);
    
    var nextChar = getFirstChar(formulaStr);
    
    //check for a left bracket
    if(nextChar == wordLeftSym)
    {
        //remove the left bracket
        formulaStr = chompOffFirstChar(formulaStr);
        
        value = wordValue(numTabs+1, assnIndex);
    }
    
    //check for a left parenthesis
    else if(nextChar == groupLeftSym)
    {
        parseTreeStr += createTabs(numTabs+1) 
            + '"' + groupLeftSym + '"' + "\n";
        
        //remove the left parenthesis
        formulaStr = chompOffFirstChar(formulaStr);
                
        value = expressionValue(numTabs+1, assnIndex);
          
        formulaStr = skipLeadingBlanks(formulaStr);
        
        nextChar = getFirstChar(formulaStr);
        
        //check for right parenthesis
        if(nextChar != groupRightSym)
        {
            updateErrorBox("missing " + groupRightSym + "\n");
        }
        else //remove right parenthesis
        {
            parseTreeStr += createTabs(numTabs+1) 
                + '"' + groupRightSym + '"' + "\n";
            
            formulaStr = chompOffFirstChar(formulaStr);
        }
    }//end else if
    
    else
    {
        updateErrorBox("unexpected character: " + nextChar + "\n");
    }
    
    if(isNegated)
    {
        value = !value;
    }
    
    //add to parse tree printout
    parseTreeStr += createTabs(numTabs) + "</factor>" + "\n";
    
    return value;
    
}//end factorValue


/*
 Return the truth value of a word.
 Assume that [ has just been chomped off.
*/
function wordValue(numTabs, assnIndex)
{
    //add to parse tree printout
    parseTreeStr += createTabs(numTabs) + "<word>" + "\n";
    
    var word = "";
    
    var nextChar = getFirstChar(formulaStr);
    
    while(nextChar != wordRightSym && formulaStr.length > 0)
    {
        word += nextChar;
        formulaStr = chompOffFirstChar(formulaStr);
        nextChar = getFirstChar(formulaStr);
    }
    
    if(nextChar != wordRightSym)
    {
        updateErrorBox("missing " + wordRightSym);
    }
    else
    {
        //remove the right bracket
        formulaStr = chompOffFirstChar(formulaStr);
    }
    
    //if the word table does not have this word yet, add it
    if( !formulaTable.hasItem(word) )
    {
        formulaTable.setItem(word, numWordsInTable);
        numWordsInTable++;
    }
    
    //get the truth value of the word from the truth table using the given assignment number
    var value;
    if(assnIndex == truthTableNotInitVal) //truth table has not been generated yet
    {
        value = startingTruthValue;
    }
    else
    {
        value = truthTable[assnIndex][formulaTable.getItem(word)];
    }
    
    //add to parseTree printout   
    parseTreeStr += createTabs(numTabs+1) + '"' + wordLeftSym + '"' + "\n";
    parseTreeStr += createTabs(numTabs+1) + word +  "\n";
    parseTreeStr += createTabs(numTabs+1) + '"' + wordRightSym + '"' + "\n";        
    parseTreeStr += createTabs(numTabs) + "</word>" + "\n";
    
    return value;
}//end wordValue


/*
 Update the error box with the latest error.
*/
function updateErrorBox(errorStr) 
{
    clearChildren("errorDiv");
    $("errorDiv").innerHTML += "<h2>Error:</h2>";
    $("errorDiv").innerHTML += "<textarea id=\"errorBox\" rows=\"2\" cols=\"38\" style = \"background-color: " + red + "\">" + (errorStr + "\n") + "</textarea>";
}


/*
 Return a string with a number of tabs for formatting.
*/
function createTabs(numTabs)
{
    var tabString = "";
    for(var i=0; i<numTabs; i++)
    {
        tabString += "|  ";
    }
    return tabString;
}


console.profileEnd(); //stop firefox javascript profiler
